Nuprl Definition : int_pi_det_fun
13,42
postcript
pdf
(
i
)
-det-fun(
j
) == (if (
i
=
0) then
j
else
i
rem
j
fi =
0)
latex
Up
rings
1
Wellformedness Lemmas
int
pi
det
fun
wf
Definitions
if
b
then
t
else
f
fi
,
(
i
=
j
)
origin
-det-fun(j) == (if (i =
0) then j else i rem j fi = 0) -det-fun(j) == (if (i = 0) then j else i rem j fi = 0) j)